This PR improves lean support for constants, using the FunctionToConstants resugaring. It removes the ad-hoc treatment of litteral consts.

Overview

A rust const can contain possibly panicking computation, like:

const C3: u32 = if true { 890 } else { 9 / 0 };

However, this is computed at compile time by rustc, so we can expect panic-freedom at extraction-time. In the Lean prelude, we add the two functions:

def isOk {α : Type} (x: Result α) : Bool := match x with
| .ok _ => true
| _ => false

def of_isOk {α : Type} (x: Result α) (h: Result.isOk x): α :=
  by cases x <;> try simp_all <;> assumption

The extracted code hardcodes a proof of panic-freedom by computation (by rfl), which should always work:

def Lean_tests.Constants.C3 :  u32 :=
  Result.of_isOk
  (do if true then pure (890 : u32) else (← (9 : u32) /? (0 : u32)))
  (by rfl)

Closes #1614